Proof Theory: The First Step into Impredicativity
Tait計算についての定義が書いてある
1966, W.W.Tait, "A non-constructive proof of Gentzen's Hauptsatz for second order predicate logic"以外でTait計算について書いてある本は私はこれしか知らない．